COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	2-IV. SEARCHING AND PATTERN MATCHING.
C00006 00003	2-V. PRIMITIVE PATTERN LANGUAGE.
C00012 ENDMK
C⊗;
2-IV. SEARCHING AND PATTERN MATCHING.
.SKIP 3
.BEGIN DOUBLE SPACE
Pattern matching is invoked by the FIND operation. FIND[<id>,<pattern>] expects
<id> to be the name of a list of clauses, and <pattern> should be a Boolean
combination of primitive patterns. These primitive patterns are described in the
next sub-section, but basically allow description of syntactic parts of clauses.

Since many of the applications of FIND are of the form FIND[CLAUSES, <pattern>],
the abbreviation, FINDC[<pattern>] has been added for this case.

Here's an example of FIND and FINDC. 

.END
.BEGIN VERBATIM
SET XX FINDC[OCR[0]];  	|OCR is a reserved word. The pattern says
			|find all clauses in the set CLAUSES which
			|have occurrences of the symbol 0.
			|In this problem 0 is a function letter.
*
DI XX;			|Display the clauses.

1 x/y=0 ⊃ x≤y;
2 x≤y ⊃ x/y=0;
3 0≤x;
4 x/x=0;
5 x/1=0;
*

SET YY FIND[XX,OCR[≤]];	|Find  clauses in XX which have occurrences
			|of the symbol '≤', and assign those clauses
			|to YY.
*
DI YY;			|Display YY.
1 x/y=0 ⊃ x≤y;
2 x≤y ⊃ x/y=0;
*

*
SET ZZ FIND[YY,OCR[/]∧OCR[=]];|Boolean combinations are allowed.
*
SET ZZ FIND[YY,LENGTH=1];|This command will locate all units in the
			 |set, YY.
.END
.SKIP 3
2-V. PRIMITIVE PATTERN LANGUAGE.
.SKIP 3
.BEGIN DOUBLE SPACE
The primitives allow description of the ancestry of a clause,
the length (number of literals) and depth (of function nesting) of clauses, besides
a very simple matching algorithm.  The matcher can  match on literals
, terms, predicate letters, negations of predicate letters, or functions symbols.


PRIMITIVES:

1) primitive for ancestry:  TREE[x]

"x" designates a clause.  TREE[x] will match any clause whose derivation tree
contains x.  N.B.  the clause x itself is considered to be derived from x.

Examples:

For example, if G1 is the name of an initial statement then :

SET YY FIND[XX,TREE[G1]]; will assign to YY all of the clauses in XX which
were derived using G1.

2) primitive for length:   LENGTH

LENGTH gives the number of literals in the clauses currently being examined.
LENGTH may be tested using one of the available relations.

Examples:

LENGTH = 1 is true if the current clause is a unit.

3) primitive for depth:    DEPTH

This primitive gives the depth of function nesting in the clause.

Example:

DEPTH > 4 is true if the depth of nesting in the current clause is greater
than 4.


Primitive relations:

Currently the only relations available are  =, >, and <.  These relations
are only to be used in comparing length and depth.

.END

.BEGIN DOUBLE SPACE

MATCHING:

4) primitive for matching: OCR

OCR is a simple matcher which expects its arguments
to be a literal, term,  predicate letter, or negation of a predicate letter.
OCR matches any clause which contains a matching construct.

Variables may appear in the pattern, in which case  a test for subsumption
determines when a match is to be successful.

Examples:

In the following, assume P, and = are predicate letters; assume x, y, and
z are variables; and assume a, b, c, d and f and g are function symbols.

OCR[P] matches P(x), P(a)⊃a=b, and ¬P(b).

OCR[¬P] matches P(a)⊃a=b and ¬P(b). Note P(a)⊃a=b matches here since the
implication really is ¬P(a) ∨ a=b;

OCR[¬=]∧¬OCR[d] would match ¬f(a,b)=c but would not match ¬f(a,b)=d.

OCR[P(x)] matches P(x),¬P(g(x)) and ¬P(a).

OCR[¬P(g(x))] matches ¬P(g(a)) but not P(g(a)) or ¬P(f(g(a),x));

OCR[f(g(x),x)] matches clauses containing say, f(g(a),a) but does not match
f(g(a),b).
.END